COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(defun flat (x u) (cond ((atom x) (cons x u))
C00008 ENDMK
C⊗;
(defun flat (x u) (cond ((atom x) (cons x u))
(t (flat (car x) (flat (cdr x) u)))))

(defun cflat (x u) (cond ((atom x) 1)
(t (plus (cflat (car x) (flat (cdr x) u)) (cflat (cdr x) u)))))

(defun dflat (x u) (cond ((atom x) 0)
(t (max (dflat (car x) (flat (cdr x) u)) (plus 1 (dflat (cdr x) u))))))

(defun rflat (x u) (cond ((atom x) 1)
(t (plus 1 (rflat (car x) (flat (cdr x) u)) (rflat (cdr x) u)))))

(defun tflat (x u) (cond ((atom x) (list (list x u (flat x u))))
(t (cons (list x u (flat x u)) (append (tflat (cdr x) u) (tflat
(car x) (flat (cdr x) u)))))))

(defun gflat (x u g h) (cond ((atom x) (g x u))
(t (h (gflat (car x) (flat (cdr x) u) g h) (gflat (cdr x) u) x u))))

(defun gflat2 (x u v g h) (cond ((atom x) (g x u v))
(t (gflat2 (car x) (flat (cdr x) u) (h (gflat2 (cdr x) u v g h) x u v) g h))))

(defun mkconscount (fn nfn)
((lambda (def)
(putprop nfn (list 'lambda (cadr def) (cc (caddr def) fn nfn)) 'expr)
) (get fn 'expr)))

(defun cc (b fn nfn) (cond ((nocons b fn) 0)
((eq (car b) 'cons) (mksum (cons 1 (cclis (cdr b) fn nfn))))
((eq (car b) fn) (mksum (cons (cons nfn (cdr b)) (cclis (cdr b) fn nfn))))
((eq (car b) 'cond) (cccond (cdr b) fn nfn))
((eq (car b) 'and) (ccand (cdr b) fn nfn))
((eq (car b) 'or) (ccor (cdr b) fn nfn))
((atom (car b)) (cclis (cdr b) fn nfn))
((eq (caar b) 'lambda)
(mksum (cons (cons (list 'lambda (cadar b) (cc (caddar b) fn nfn)) (cdr b))
(cclis (cdr b) fn nfn))))))

(defun nocons (b fn) (and (not (eq b 'cons)) (not (eq b fn)) (or (atom b)
(and (nocons (car b) fn) (nocons (cdr b) fn)))))

(defun cclis (u fn nfn) (cond ((null u) nil) (t (cons (cc (car u) fn nfn)
(cclis (cdr u) fn nfn)))))

(defun cccond (u fn nfn) (cond ((eq (caar u) t) (cc (cadar u) fn nfn))
(t (mksum (list (cc (caar u) fn nfn)
(list 'cond (list (caar u) (cc (cadar u) fn nfn))
(list 't (cccond (cdr u) fn nfn))))))))

(defun ccand (u fn nfn) (cond ((null u) 0)
(t (mksum (cons (cc (car u) fn nfn) (list 'cond (list (car u)
(ccand (cdr u) fn nfn)) (list 't 0)))))))

(defun ccor (u fn nfn) (cond ((null u) 0)
(t (mksum (cons (cc (car u) fn nfn) (list 'cond (list (car u) 0)
(list 't (ccor (cdr u) fn nfn))))))))

(defun mksum (u) (mksum1 (mksum2 u)))

(defun mksum1 (u) (cond ((null u) 0) ((null (cdr u)) (car u))
(t (cons 'plus u))))

(defun mksum2 (u) (cond ((null u) nil) ((equal (car u) 0) (mksum2 (cdr u)))
(t (cons (car u) (mksum2 (cdr u))))))

(defun alt (u)
(cond ((or (null u) (null (cdr u))) u)
(t (cons (car u) (alt (cddr u))))))

(defun subst1 (x y z)
(cond ((atom z) (cond ((equal z y) x) (t z)))
(t ((lambda (z1 z2) (cond ((and (equal z1 (car z)) (equal z2 (cdr z))) z)
(t (cons z1 z2)))) (subst1 x y (car z)) (subst1 x y (cdr z))))))

(defun itflat (x u state) (cond ((atom x) (itflat1 (cons x u) state))
(t (itflat (cdr x) u (cons 'a (cons (car x) state))))))

(defun itflat1 (value state) (cond ((null state) value)
((eq (car state) 'a) (itflat (cadr state) value (cons 'b (cddr state))))
((eq (car state) 'b) (itflat1 value (cdr state)))))

(setq base (setq ibase 10.))

(defun itf91 (n state) (cond ((greaterp n 100.) (itf911 (difference n 10.) state))
(t (itf91 (plus n 11.) (cons 'a state)))))

(defun itf911 (value state) (cond ((null state) value)
((eq (car state) 'a) (itf91 value (cons 'b (cdr state))))
((eq (car state) 'b) (itf911 value (cdr state)))))

(defun itf91a(n state) (cond ((greaterp n 100.) (itf911a (difference n 10.) state))
(t (itf91a (plus n 11.) (cons 'a state)))))

(defun itf911a (value state) (cond ((null state) value)
((eq (car state) 'a) (itf91a value (cdr state)))))